Cmd:Type, P:(chain_sys(Cmd)).
(cmd:Cmd. P(csinput(cmd)))
 (from:Id, cmds:(Cmd List). P(csupdate(from;cmds)))
 {x:chain_sys(Cmd). P(x)} 

latex

Definitions	t  T, type List, Id, f(a), x(s), x:AB(x), x:A. B(x), inl x , inr x , x:A  B(x), left + right, chain_sys(Cmd), csinput(cmd), csupdate(from;cmds), Type, s = t, , strong-subtype(A;B), P  Q, {T}
Lemmas	Id wf, csupdate wf, csinput wf, chain sys wf